package autoz.czt.visitor;

import java.util.List;

import net.sourceforge.czt.base.ast.Term;
import net.sourceforge.czt.session.CommandException;
import net.sourceforge.czt.session.FileSource;
import net.sourceforge.czt.session.Key;
import net.sourceforge.czt.session.Markup;
import net.sourceforge.czt.session.SectionManager;
import net.sourceforge.czt.session.Source;
import net.sourceforge.czt.typecheck.z.ErrorAnn;
import net.sourceforge.czt.typecheck.z.impl.Factory;
import net.sourceforge.czt.z.ast.Spec;
import net.sourceforge.czt.z.ast.ZFactory;
import net.sourceforge.czt.z.impl.ZFactoryImpl;

/**
 * This class is not intended to be extended.
 * @author jw
 *
 */
public abstract class CZTUtils {

	public static Spec parseSpec(String file, SectionManager manager) throws CommandException {
		Source source = new FileSource(file);
		source.setMarkup(Markup.LATEX);
		
		manager.put(new Key<Source>(file, Source.class), source);
		
//		System.out.println(manager.getProperty("czt.path"));
		//TODO calc the path / pass as parameter
//		manager.setProperty("czt.path", "/Users/jimmy/Documents/Projects/autozmarkii/doc/ExampleUML"); 
		
		
		return manager.get(new Key<Spec>(file, Spec.class));
	}
	
	public static List<? extends ErrorAnn> typecheck(Term term, SectionManager manager){
		ZFactory zFactory = new ZFactoryImpl();
//		TypeChecker typeChecker = new TypeChecker(new Factory(zFactory), manager, false);
		NewErrorVisitor typeChecker = new NewErrorVisitor(new Factory(zFactory), manager);
		
		typeChecker.setUseNameIds(false);
		term.accept(typeChecker);
		
		return typeChecker.errors();
	}

}
